\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Definition} \coqdocvar{empty\_state} : \coqdocvar{State} := \coqdockw{fun} \coqdocvar{\_} \ensuremath{\Rightarrow} \coqdocvar{None}.\coqdoceol
\end{coqdoccode}